Inference at * 2 
Iof proof for Lemma decidable-filter:



1. T : Type
2. T List
3. u : T
4. v : T List
5. P:({x:T| (x  v)} ).
5. (xv. Dec(P(x)))  (L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x)))))
6. P : {x:T| (x  [u / v])} 
7. x[u / v]. Dec(P(x))
  L':T List. (L'  [u / v] & (x:T. (x  L')  ((x  [u / v]) & P(x)))) 

latex

 by ((InstHyp [P] (-3)) 
CollapseTHEN (MaAuto)) 

latex

C1: .....wf..... NILNIL

C1:   P  {x:T| (x  v)} 
C2: .....antecedent..... NILNIL

C2:   xv. Dec(P(x))
C3: 

C3: 8. L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x))))
C3:   L':T List. (L'  [u / v] & (x:T. (x  L')  ((x  [u / v]) & P(x))))
C.

Definitions

suptype(S; T), filter(P;l), SQType(T), s ~ t, S  T, Void, #$n, <a, b>, {T}, ||as||, , l[i], last(L), [], |r|, |g|, |p|, x,y:A//B(x;y), , {i..j}, Atom, , (xL.P(x)), x f y, A c B, a < b, a <p b, a  b, a ~ b, b | a, b, A  B, A, False, a < b, t  T, [car / cdr], {x:A| B(x)} , xL. P(x), Dec(P), P  Q, left + right, , L1  L2, P  Q, increasing(f;k), s = t, x:A. B(x), x:A. B(x), type List, Type, P  Q, P  Q, x:AB(x), P & Q, x:A  B(x), x(s), f(a), (x  l)

Lemmas

false wf, guard wf, not wf, decidable wf, member wf, subtype rel wf, nat wf, length wf1, select wf, sublist wf, iff wf, cons member, rev implies wf, l member wf